(set-logic QF_UF)
(declare-sort S0 0)
(declare-sort S1 0)
(declare-sort S2 0)
(declare-fun v0 () S0)
(declare-fun v2 () S0)
(declare-fun v3 () S1)
(declare-fun v4 () S1)
(declare-fun v5 () S1)
(declare-fun f2 (S0 S1) S2)
(declare-fun f3 (S1 S2 S0) S1)
(assert (let ((e10 (! v5 :named term10))) (let ((e11 (! (f2 v2 v3) :named term11))) (let ((e14 (! (f3 v4 e11 v0) :named term14))) (let ((e15 (! e10 :named term15))) (let ((e28 (! (= e14 v3) :named term28))) (let ((e147 (! (= e28 false) :named term147))) (let ((e168 (! (xor true e147) :named term168))) (let ((e179 (! e168 :named term179))) (! (=> e179 false) :named term183))))))))))
(check-sat)
(get-value ( term15))
